{
module Zeno.FLParser ( parseFL, Lemma (..) ) where

import Prelude ()
import StdImports

import Zeno.Term
import Zeno.Clause
import Zeno.Type
}

%name flParser
%tokentype { Token }

%token
  var         { TokenVar $$ }
  '.'         { TokenEnd }
  ':'         { TokenType }
  ':-'        { TokenImpl }
  '->'        { TokenArr }
  ','         { TokenComma }
  '('         { TokenOP }
  ')'         { TokenCP }
  '='         { TokenEq }
    
%%

Lemmas
  : {- empty -}                       { [] }
  | Lemmas Lemma                      { $2 : $1 }
  
Lemma
  : var TypedNames Equality Conds '.' { Lemma $1 $2 $3 $4 }

TypedNames
  : {- empty -}                       { [] }
  | TypedNames TypedName              { $2 : $1 }
  
TypedName
  : '(' var ':' Type ')'              { ($2, $4) }
  
Type 
  : var                               { TypeVar $1 }
  | var '->' Type                     { FunType (TypeVar $1) $3 }
  | '(' Type ')' '->' Type            { FunType $2 $5 }
  | '(' Type ')'                      { $2 }
  
Term
  : var                               { Var $1 }
  | Term var                          { App $1 (Var $2) }
  | Term '(' Term ')'                 { App $1 $3 }
  | '(' Term ')'                      { $2 }
  
Equality 
  : Term '=' Term                     { ($1, $3) }
  | Term                              { ($1, (Var "True")) }
  
Conds
  : {- empty -}                       { [] }
  | ':-' Equality Conj                { $2 : $3 }
  
Conj
  : {- empty -}                       { [] }
  | Conj ',' Equality                 { $3 : $1 }
  
{
happyError :: [Token] -> a
happyError tokens = error $ "Parse error\n" ++ (show tokens)

data Lemma 
  = Lemma   { lemmaName :: String,
              lemmaVariables :: [(String, Type String)],
              lemmaEquality :: Equality String,
              lemmaConditions :: [Equality String] }

data Token
  = TokenVar String
  | TokenEnd
  | TokenType
  | TokenOP 
  | TokenCP
  | TokenEq 
  | TokenImpl
  | TokenArr
  | TokenComma
  deriving Show
  
isWMLAlpha :: Char -> Bool
isWMLAlpha '\'' = True
isWMLAlpha c = isAlpha c 

isWMLAlphaNum c = isWMLAlpha c || isDigit c
  
flLexer :: String -> [Token]
flLexer [] = []
flLexer ('{':'-':' ':'Z':'e':'n':'o':cs) = lexer cs
flLexer (_:cs) = flLexer cs

lexer :: String -> [Token]
lexer [] = []
lexer ('\n':cs) = lexer cs
lexer (c:cs) 
  | isSpace c = lexer cs
  | isWMLAlpha c = lexVar (c : cs)
lexer ('.':cs) = TokenEnd : lexer cs
lexer (',':cs) = TokenComma : lexer cs
lexer ('-':'>':cs) = TokenArr : lexer cs
lexer (':':'-':cs) = TokenImpl : lexer cs
lexer (':':cs) = TokenType : lexer cs
lexer ('(':cs) = TokenOP : lexer cs
lexer (')':cs) = TokenCP : lexer cs
lexer ('=':cs) = TokenEq : lexer cs
lexer ('-':'}':cs) = flLexer cs 
lexer cs = error $ "Unrecognized symbol " ++ take 1 cs

lexVar cs =
  case span isWMLAlphaNum cs of
    (var, rest) -> TokenVar var : lexer rest
    
parseFL :: String -> [Lemma]
parseFL = flParser . flLexer
}
